R:Realizer. R-Feasible(R)  (es:ES. Possible(R;es)) 

latex

Definitions	x:A. B(x), P  Q, x:A. B(x), P & Q, P  Q, P  Q, t  T, Prop, Possible(R;es), 1of(t), A & B, PossibleWorld(D;w)
Lemmas	R-Feasible wf, event system wf, R-possible wf, es realizer wf, R-Feasible-Dsys, d-feasible-world, R-Dsys wf, w-es wf, possible-world wf, fair-fifo wf